Require Export Matrix.MMat.MMatrix_Module.

(* the definition of blocl matrix equivalence *) 
Check MM_eq. (* Mat (Mat ?A ?m ?n) ?m2 ?n2 -> Mat (Mat ?A ?m ?n) ?m2 ?n2 -> Prop *)
(* Notation == *)

(* block matrix -> matrix *)
Check MM_to_M. (* : Mat (Mat ?A ?m ?n) ?m2 ?n2 -> Mat ?A (?m2 * ?m) (?n2 * ?n) *)

(* MM_to_M(block zero matrix) === zero matrix *) 
Check MM_to_M_MO : forall (A : Set) (Zero : A)(m n m2 n2 : nat),
    MM_to_M(MO (Mat A m n)(MMat_def.mZero Zero m n) m2 n2) 
    === MO A Zero (m2 * m) (n2 * n).

(* MM_to_M( - MA ) === - (MM_to_M MA), where MA is a block matrix *)
Check MM_to_M_matrix_map : forall (A : Set) (m n : nat) (f1 : A -> A) (m2 n2 : nat) (ma : Mat (Mat A m n) m2 n2),
       MM_to_M (matrix_map (Mat A m n) (matrix_map A f1) ma) ===
       matrix_map A f1 (MM_to_M ma).

(* MA == MB <-> MM_to_M A === MM_to_M B, where MA and MB are block matrices *)
Check MM_to_M_M_eq: forall (A : Set) (m n m2 n2 : nat) (ma mb : 
      Mat (Mat A m n) m2 n2),ma == mb <-> MM_to_M ma === MM_to_M mb.

(* MM_to_M( MA +/- MB ) === (MM_to_M MA) +/- (MM_to_M MB), 
    where MA and MB are block matrices *)
Check MMf_eq_Mf: forall (A : Set) (Zero : A) (m n : nat) (f : A -> A -> A) 
         (m2 n2 : nat) (me mf : Mat (Mat A m n) m2 n2),
       (forall a : A, f a Zero = a) ->
       MM_to_M (matrix_each (Mat A m n) (matrix_each A f) me mf) ===
       matrix_each A f (MM_to_M me) (MM_to_M mf).

(* MM_to_M ( - MA ) === - (MM_to_M MA) *)
Check MMm_eq_Mm: forall (A : Set) (m n : nat) (f1 : A -> A) (m2 n2 : nat) (me : Mat (Mat A m n) m2 n2),
       Mat (Mat A m n) m2 n2 ->
       MM_to_M (matrix_map (Mat A m n) (matrix_map A f1) me) ===
       matrix_map A f1 (MM_to_M me).

(* MA × MB *)
Check mmatrix_mul.

(* MM_to_M( MA × MB ) === (MM_to_M MA) × (MM_to_M MB) *)
Check MMmul_eq_Mmul : forall (A : Set) (Zero : A) (add mul : A -> A -> A) (m n p m2 n2 p2 : nat)
         (me : Mat (Mat A m n) m2 n2) (mf : Mat (Mat A n p) n2 p2),
       (forall a1 b : A, mul a1 b = mul b a1) ->
       (forall a1 : A, add Zero a1 = a1) ->
       (forall a1 : A, add a1 Zero = a1) ->
       (forall a1 b c : A, add a1 (add b c) = add (add a1 b) c) ->
       MM_to_M (mmatrix_mul A Zero add mul m n p me mf) ===
       matrix_mul A Zero add mul (MM_to_M me) (MM_to_M mf).

(* MA + MB == MB + MA *)
Check mmatrix_each_comm .

(* MA + MB + MC == MA + ( MB + MC ) *)
Check mmatrix_assoc.

(* O + MA == MA, where O is a block zero matrix *)
Check mmatrix_add_zero_l.

(* MA + O == MA *)
Check mmatrix_add_zero_r.

(* MA - MB == -(MB - MA) *)
Check mmatrix_sub_opp.

(* MA - MB - MC == MA - (MB + MC) *)
Check mmatrix_sub_assoc.

(* O - MA == - MA *)
Check mmatrix_sub_zero_l.

(* MA - O == MA *)
Check mmatrix_sub_zero_r.

(* MA - MA == O *)
Check mmatrix_sub_self.

(* (MA +/- MB)× MC == MA × MC +/- MB × MC *)
Check mmatrix_mul_distr_l.

(* MA × (MB +/- MC) == MA × MB +/- MA × MC *)
Check mmatrix_mul_distr_r.

(* O × MA == O *)
Check mmatrix_mul_zero_l.

(* MA × O == O *)
Check mmatrix_mul_zero_r.

(* MA × MB × MC == MA × ( MB × MC )*)
Check mmatrix_mul_assoc.

(* transpose of block matrix TM(A) *)
Check mmtrans: forall A : Set,
       A -> forall m n m2 n2 : nat, Mat (Mat A m n) m2 n2 -> Mat (Mat A n m) n2 m2.

(* TM(MA × MB) == TM(MB) × TM(MA) *)
Check mmtrans_mul.

(* MM_to_M( TM(MA)) === T( MM_to_M MA ) *)
Check MMtrans_eq_Mtrans.

(* TM(TM(MA)) == MA *)
Check mmtrans_same.

(* TM( MA +/- MB ) == TM(MA) +/- TM(MB) *)
Check mmteq_f.









